\begin{tabbing}
$\forall$$E$:Type, ${\it pred?}$:($E$$\rightarrow$($E$+Unit)), $a$, $b$, $e$:$E$.
\\[0ex]SWellFounded($\neg$first($y$) \& $x$ $=$ pred($y$) $\in$ $E$)
\\[0ex]$\Rightarrow$ (\=$a$ before $b$ $\in$ eventlist(${\it pred?}$;$e$)\+
\\[0ex]$\Leftrightarrow$
\\[0ex]($a$ (($\lambda$$x$,$y$. $\neg$first($y$) \& $x$ $=$ pred($y$) $\in$ $E$)$^{\mbox{\scriptsize $\ast$}}$) $e$)
\\[0ex]\& ($b$ (($\lambda$$x$,$y$. $\neg$first($y$) \& $x$ $=$ pred($y$) $\in$ $E$)$^{\mbox{\scriptsize $\ast$}}$) $e$)
\\[0ex]\& ($a$ $\lambda$$x$,$y$. $\neg$first($y$) \& $x$ $=$ pred($y$) $\in$ $E$\^{}+ $b$))
\-
\end{tabbing}